$\forall$$A$:Realizer, $k$:Knd.
\\[0ex]R{-}Feasible($A$)
\\[0ex]$\Rightarrow$ isrcv($k$)
\\[0ex]$\Rightarrow$ $k$ $\in$ dom(R{-}da($A$;source(lnk($k$))))
\\[0ex]$\Rightarrow$ R{-}da($A$;source(lnk($k$)))($k$) $\subseteq\rho$ Valtype(R{-}da($A$;destination(lnk($k$)));$k$)